#include "LADSUtil/exceptions.h"

#include "ComboReduct/combo/assumption.h"
#include <iostream>
#include <vector>

namespace combo {
  typedef vtree::iterator pre_it;
  typedef vtree::sibling_iterator sib_it;

  void insert_assumption(vtree& tr, vtree::iterator assum_it) {
    typedef LADSUtil::lexicographic_subtree_order<vertex> Comp;
    pre_it main_tree = tr.begin();
    cassert(TRACE_INFO, tr.is_valid(main_tree), "vtree ins't valid (insert_assumption).");
    int max_pos = tr.number_of_siblings(main_tree);
    if(max_pos>1) {
      int min_pos = 1;
      int diff = (max_pos-min_pos)/2;
      int cur_pos = min_pos + diff;
      sib_it cur_sib = main_tree;
      cur_sib += cur_pos;
      Comp comp;
      while(min_pos<max_pos) {
	if(comp(pre_it(cur_sib), assum_it)) {
	  min_pos = cur_pos+1;
	  diff = 1+(max_pos-min_pos)/2;
	  cur_pos += diff;
	  cur_sib += diff;
	}
	else if(comp(assum_it, pre_it(cur_sib))) {
	  max_pos = cur_pos-1;
	  diff = 1+(max_pos-min_pos)/2;
	  cur_pos -= diff;
	  cur_sib -= diff;
	}
	else return;
      }
      if(max_pos<min_pos)
	tr.insert_subtree_after(cur_sib, assum_it);
      else if(min_pos==max_pos) {
	if(comp(pre_it(cur_sib), assum_it)) {
	  tr.insert_subtree_after(cur_sib, assum_it);
	}
	else if(comp(assum_it, pre_it(cur_sib))) {
	  tr.insert_subtree(cur_sib, assum_it);
	}
      }
      else cassert(TRACE_INFO, false, "should never get here (insert_assumption).");
    }
    else tr.insert_subtree_after(main_tree, assum_it);
  }

  bool find_vertices_in_assumptions(const vtree& tr, vertex v,
				    std::vector<vtree::iterator>& res) {
    pre_it tr_it = tr.begin();
    cassert(TRACE_INFO, tr.is_valid(tr_it), "vtree isn't valid (find_vertices_in_assumptions).");
    pre_it assum_it = tr.next_sibling(tr_it);
    bool is_there = false;
    if(tr.is_valid(assum_it)) {
      for(; assum_it != tr.end(); ++assum_it) {
	if(*assum_it == v) {
	  res.push_back(assum_it);
	  is_there = true;
	}
      }
    }
    return is_there;
  }
  
  bool equal_assumptions(const vtree& tr1, const vtree& tr2) {
    cassert(TRACE_INFO, !tr1.empty() && !tr2.empty(), "assumptions should not be empty (equal_assumptions).");
    sib_it assum1 = tr1.next_sibling(tr1.begin());
    sib_it assum2 = tr2.next_sibling(tr2.begin());
    if(tr1.is_valid(assum1) && tr2.is_valid(assum2)) {
      for(; assum1 != tr1.end() && assum2 != tr2.end(); ++assum1, ++assum2)
	if(!tr1.equal_subtree(assum1, assum2))
	  return false;
      if(assum1==tr1.end() && assum2==tr2.end())
	return true;
      else return false;
    }
    else return true;
  }

  void delete_all_assumptions(vtree& tr) {
    cassert(TRACE_INFO, !tr.empty(), "vtree should not be empty (delete_all_assumptions).");
    sib_it assum = tr.next_sibling(tr.begin());
    if(tr.is_valid(assum))
      for(; assum != tr.end();) 
	assum = tr.erase(assum);
  }

  bool test() {
    return true;
  }

}//~namespace combo
